(declare-sort S0 0)

(declare-sort S1 0)

(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const r0 Real)
(declare-const r1 Real)
(declare-const v3 Bool)
(declare-const r3 Real)
(declare-const r4 Real)
(declare-const v4 Bool)
(declare-const v5 Bool)
(push)
(declare-const v6 Bool)
(pop)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const r5 Real)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const r6 Real)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const S0-0 S0)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const r7 Real)
(declare-const r8 Real)
(assert (or (not v0) v0 (distinct v2 (>= r0 r1))))
(assert (or (< r0 r4 (- 3)) (= r5 r3 r5) (or v5 v3 v1 (and v1 (>= r0 r1)) (not v0) v3 (not v0) v5 (>= r0 r1))))
(assert (or (distinct v2 (>= r0 r1)) v2 (and v1 (>= r0 r1))))
(assert (or v9 (not v0) v14))
(assert (or v5 (= r5 r3 r5) v0))
(assert (or v2 v11 (< (/ r3 (- 3)) (- (- r0)))))
(assert (or (< r0 r4 (- 3)) (>= r0 r1) (distinct v2 (>= r0 r1))))
(assert (or (or v5 v3 v1 (and v1 (>= r0 r1)) (not v0) v3 (not v0) v5 (>= r0 r1)) v14 (= r5 r3 r5)))
(assert (or v11 (< r0 r4 (- 3)) (and v1 (>= r0 r1))))
(assert (or v11 (< (/ r3 (- 3)) (- (- r0))) v0))
(assert (or v2 (or v5 v3 v1 (and v1 (>= r0 r1)) (not v0) v3 (not v0) v5 (>= r0 r1)) (distinct v2 (>= r0 r1))))
(assert (or (distinct S0-0 S0-0) (and v8 v3 v4 (>= r0 r1) v5) v5))
(assert (or v8 (and v8 v3 v4 (>= r0 r1) v5) (distinct S0-0 S0-0)))
(assert (or v5 (or v5 v3 v1 (and v1 (>= r0 r1)) (not v0) v3 (not v0) v5 (>= r0 r1)) (distinct v2 (>= r0 r1))))
(assert (or (not v0) v2 (not v0)))
(assert (or (or v5 v3 v1 (and v1 (>= r0 r1)) (not v0) v3 (not v0) v5 (>= r0 r1)) v9 v0))
(assert (or v13 (and v1 (>= r0 r1)) v14))
(assert (or (< r0 r4 (- 3)) (< (/ r3 (- 3)) (- (- r0))) v0))
(assert (or v8 v8 v5))
(assert (or (and v8 v3 v4 (>= r0 r1) v5) v2 v13))
(assert (or (and v8 v3 v4 (>= r0 r1) v5) (= r5 r3 r5) (and v8 v3 v4 (>= r0 r1) v5)))
(assert (or v8 (= r5 r3 r5) v11))
(assert (or v5 v13 v14))
(assert (or (distinct v2 (>= r0 r1)) v2 v11))
(assert (or (< (/ r3 (- 3)) (- (- r0))) v2 (= r5 r3 r5)))
(assert (or (and v1 (>= r0 r1)) v5 (< r0 r4 (- 3))))
(assert (or v8 v8 (distinct v2 (>= r0 r1))))
(assert (or (= r5 r3 r5) (>= r0 r1) v2))
(assert (or (not v0) v8 v11))
(assert (or (or v5 v3 v1 (and v1 (>= r0 r1)) (not v0) v3 (not v0) v5 (>= r0 r1)) v8 v9))
(assert (or (distinct S0-0 S0-0) (>= r0 r1) (and v8 v3 v4 (>= r0 r1) v5)))
(assert (or (< r0 r4 (- 3)) v11 v13))
(assert (or v2 (and v1 (>= r0 r1)) (>= r0 r1)))
(assert (or (and v8 v3 v4 (>= r0 r1) v5) (and v8 v3 v4 (>= r0 r1) v5) v0))
(assert (or v5 (or v5 v3 v1 (and v1 (>= r0 r1)) (not v0) v3 (not v0) v5 (>= r0 r1)) (or v5 v3 v1 (and v1 (>= r0 r1)) (not v0) v3 (not v0) v5 (>= r0 r1))))
(assert (or v9 v11 (< (/ r3 (- 3)) (- (- r0)))))
(assert (or (< (/ r3 (- 3)) (- (- r0))) v0 v9))
(assert (or v9 (distinct v2 (>= r0 r1)) v8))
(assert (or (and v8 v3 v4 (>= r0 r1) v5) (>= r0 r1) v0))
(assert (or v14 v9 (distinct v2 (>= r0 r1))))
(assert (or (not v0) v5 (and v1 (>= r0 r1))))
(assert (or (and v1 (>= r0 r1)) (distinct S0-0 S0-0) v5))
(assert (or (distinct v2 (>= r0 r1)) v14 (distinct v2 (>= r0 r1))))
(assert (or (< (/ r3 (- 3)) (- (- r0))) v0 (not v0)))
(assert (or v5 v2 (>= r0 r1)))
(assert (or (and v1 (>= r0 r1)) v13 v8))
(assert (or (< (/ r3 (- 3)) (- (- r0))) v14 (not v0)))
(assert (or (and v8 v3 v4 (>= r0 r1) v5) (not v0) (and v8 v3 v4 (>= r0 r1) v5)))
(assert (or (< r0 r4 (- 3)) (< r0 r4 (- 3)) (>= r0 r1)))
(assert (or (and v8 v3 v4 (>= r0 r1) v5) (and v8 v3 v4 (>= r0 r1) v5) (not v0)))
(assert (or (>= r0 r1) (< (/ r3 (- 3)) (- (- r0))) (< (/ r3 (- 3)) (- (- r0)))))
(assert (or v8 (< r0 r4 (- 3)) v11))
(assert (or v9 v2 v11))
(assert (or (= r5 r3 r5) v2 (< (/ r3 (- 3)) (- (- r0)))))
(assert (or v5 (= r5 r3 r5) v0))
(assert (and (or (distinct S0-0 S0-0) (>= r0 r1) (and v8 v3 v4 (>= r0 r1) v5)) (or v5 v2 (>= r0 r1)) (or (< (/ r3 (- 3)) (- (- r0))) v0 (not v0)) (or (not v0) v5 (and v1 (>= r0 r1))) (or v5 (or v5 v3 v1 (and v1 (>= r0 r1)) (not v0) v3 (not v0) v5 (>= r0 r1)) (or v5 v3 v1 (and v1 (>= r0 r1)) (not v0) v3 (not v0) v5 (>= r0 r1))) (or (or v5 v3 v1 (and v1 (>= r0 r1)) (not v0) v3 (not v0) v5 (>= r0 r1)) v8 v9) (or v9 v11 (< (/ r3 (- 3)) (- (- r0))))))
(assert (=> (or v2 v11 (< (/ r3 (- 3)) (- (- r0)))) (or (distinct v2 (>= r0 r1)) v14 (distinct v2 (>= r0 r1)))))
(assert (or (or (not v0) v8 v11) (or (< (/ r3 (- 3)) (- (- r0))) v2 (= r5 r3 r5))))
(check-sat)
